es:event_system{i:l}, e:es-E(es).
(es-first(es; e))
 sqequal(es_state_when(es; e); (x,t. es_init(es)(loc(e),x,t + es-time(es; e)))) 

latex

Definitions	es-E(es), event_system{i:l}, es_state_when(es; e), left + right, Unit, P  Q, P  Q, x:A  B(x), x:AB(x), es-first(es; e), prop{i:l}, s = t, , b, b, x:A. B(x), t  T, es_time(es), s+r, let x = a in b(x), loc(e), es-time(es; e), A, P  Q, False
Lemmas	assert wf, not wf, bnot wf, bool wf, es-first wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, es-E wf